00100	GIVEAX(R1,(∀ U)(∀ F)(ISMAP F ∧ U ⊂ DOMAIN F
00200				⊃
00300		ISMAP RESTRICT(F,U) ∧ DOMAIN RESTRICT(F,U) = U
00400		∧ RANGE RESTRICT(F,U) = RANGE F
00500		∧ (∀ X)(X ε U ⊃ β(RESTRICT(F,U),X) = β(F,X))));
00600	
00700	GIVEAX(R2,(∀ F)(∀ G)(ISMAP F ∧ ISMAP G ⊃ ISMAP CHANGE(F,G)
00800		∧ DOMAIN CHANGE(F,G) = DOMAIN F ∪ DOMAIN G
00900		∧ RANGE CHANGE(F,G) = RANGE F ∪ RANGE G
01000		∧ (∀ X)(X ε DOMAIN CHANGE(F,G) ⊃
01100			β(CHANGE(F,G),X) = IF X ε DOMAIN G THEN β(G,X)
01200					ELSE β(F,X))));
01300	
01400	GIVEAX(R3,(∀ X)(∀ Y)(ISMAP MAPTO(X,Y)
01500		∧ DOMAIN MAPTO(X,Y) = UNITSET X
01600		∧ RANGE MAPTO(X,Y) = UNITSET Y
01700		∧ β(MAPTO(X,Y),X) = Y));
01800	
01900	GIVEAX(R4,(∀ F)(∀ X)(∀ Y)( ISMAP F ⊃ A(X,Y,F) 
02000					= CHANGE(F,MAPTO(X,Y));
02100	
02200	GIVEAX(R5,(∀ U)(ISSET U ⊃ ISMAP NULLMAP U 
02300				∧ DOMAIN NULLMAP U = NULLSET
02400				∧ RANGE NULLMAP U = U));
02500	
02600	GIVEAX(R6,(∀ F)(ISMAP F ⊃ ISMAP CONTRACT F
02700				∧ DOMAIN CONTRACT F = DOMAIN F
02800				∧ RANGE CONTRACT F = RRANGE F
02900				∧ (∀ X)(X ε DOMAIN F
03000					⊃ β(CONTRACT F,X) = β(F,X))));